1. Field of the Invention
The present invention relates in general to the field of shared memory multiprocessor computer systems, and more particularly to a verification system and method for shared memory multiprocessor memory consistency models.
2. Description of the Related Art
Shared memory multiprocessor computer system architectures have become a common solution for complex computing needs, such as are often encountered in computer network servers and telecommunications applications. A typical shared memory multiprocessor computing system includes two or more processors that access shared memory. The same physical address on different processors typically refers to the same location in the shared memory. In shared memory architectures, a memory consistency model typically specifies the semantics of memory operations to coordinate accesses by multiple processors to the shared memory. A memory model effectively establishes a contract between the programmer and the hardware. Thus, both programs and hardware in a shared memory multiprocessor system must be correct with respect to the memory model definition for proper operation. Memory models can have a significant impact on ease of programming and optimizations performable by the hardware or the compiler.
One example of a memory consistency model for shared memory multiprocessor machines is the Total Store Order (“TSO”) memory model developed by Sun Mircrosystems, Inc. The TSO memory model specification defines the semantics of load, store and atomic memory operations in uniprocessor or multiprocessor systems from the point of view of program results. TSO defines two types of orders over the set of memory operations. A single partial order, or memory order, conforms to the order in which operations are performed by memory in real time. A per processor total order, or program order, denotes the sequence in which the processor logically executes instructions. Memory operations are ordered by six TSO rules or axioms: the Order rule states that the partial order is total over all stores; the Atomicity rule states that a swap is atomic with respect to other stores; the Termination rule states that all stores and swaps eventually terminate; the Value rule states that the value of a load is the value written by the most recent store to that location; the LoadOp rule states that if an operation follows a load in per processor total order then it must also follow the load in single partial order; and the StoreStore rule states that if two stores appear in a particular order in per processor total order, then they must also appear in the same order in single partial order. The rules are applied to model instructions from processors to provide a set of event orders for coordinated accesses by the processors to the shared memory.
One difficulty with shared memory multiprocessor architectures is that design problems or bugs are difficult to find, isolate and correct. Undetected bugs result in improper operations that often lead to system failures and that delay new design releases or, worse, require post-release patches. One way of verifying a memory model is to use specific algorithms targeted to test the model under test, but these specific algorithm techniques are typically incomplete in their coverage and hence cannot provide high confidence. Another approach is to use random program generators to stress the model under test but random program generators have a major limitation in that they cannot be compared against the architectural model. If data races are generated by random instructions, the results of the instructions are difficult to check unless obvious problem manifestations arise like a system hang or monitor error in simulation. In order to avoid data races, random generation verification typically places accesses in shared memory in a way that allows reasoning through the outcome of the program to check the results, thus limiting the randomness of the program to specific idioms.